\begin{tabbing}
$\forall$\=${\it es}$:ES, ${\it Cmd}$:Type, ${\it Sys}$:AbsInterface(chain\_sys(${\it Cmd}$)), ${\it Config}$:AbsInterface(chain\_config()),\+
\\[0ex]$u$:(\{$e$:E(${\it Sys}$)$\mid$ $\uparrow$csupdate?(${\it Sys}$($e$))\} $\rightarrow$\{$e$:E$\mid$ ($\uparrow$($e$ $\in_{b}$ ${\it Sys}$)) $\vee$ ($\uparrow$($e$ $\in_{b}$ ${\it Config}$))\} ).
\-\\[0ex]update{-}antecedent\{i:l\}(${\it es}$;${\it Cmd}$;${\it Sys}$;${\it Config}$;$u$)
\\[0ex]$\Rightarrow$ ${\it Sys}$ $\cap$ ${\it Config}$ = 0
\\[0ex]$\Rightarrow$ (cr{-}antecedent\{i:l\}(${\it es}$;${\it Config}$;${\it Cmd}$;${\it Sys}$;$u$) $\in$ sys{-}antecedent(${\it es}$;${\it Sys}$(valid)))
\end{tabbing}